es:event_system{i:l}. 
es-Trans(es)
 i:Idk:Kndkindcase(k; a.(es-V(es)(i,a)); l,t.(es-M(es)(l,t)))es_state(es; i)es_state
 (es; i) 

latex

Definitions	t  T, f(a), rationals, x:AB(x), Id, x:A. B(x), subtype(S; T), EState(T), b, IdLnk, Type, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t)), Knd, suptype(S; T), P  Q, es-T(es), es_vartype(es; i; x), es-Trans(es), es_state(es; i), es-M(es), es-V(es), x:A  B(x), event_system{i:l}
Lemmas	event system wf, Knd wf, kindcase wf, IdLnk wf, EState wf, Id wf, rationals wf